#include "SeqSolver.h"
#include <iostream>
#include <fstream>

int main(int argc, char** argv) {
    
    if(argc != 2) {
        std::cerr << "Usage: " << argv[0] << " <input cnf file>" << "\n";
        return -1;
    }
    
    std::ifstream f(argv[1]);
    std::string s;
    while(std::getline(f, s)) {
        if(s[0] == 'p') break;
    }
    
    bool newClause = true;
    Clause* clause = 0;
    Problem problem;
    while(f) {
        int i;
        f >> i;
        if(i == 0) { 
            if(clause) problem.addClause(clause);
            newClause = true; 
        }
        else { 
            if(newClause == true) {
                clause = new Clause();
                clause->addVariableParity(i);
                newClause = false;
            } else {
                clause->addVariableParity(i);
            }
        }
    }
    SATSeqSolver solver;
    solver.initializeProblem(problem);
    solver.solve();
    return 0;
}
